Nuprl Lemma : rem_bounds_2
13,42
postcript
pdf
a
:{...0},
n
:
. (0
(
a
rem
n
) ) & ((
a
rem
n
) > (-
n
))
latex
Up
int
2
,
int
2
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
False
,
P
Q
,
A
,
A
B
,
i
>
j
,
,
{...
i
}
Lemmas
int
lower
wf
,
nat
plus
wf
origin
a:{...0}, n:
. (0 
(a rem n) ) & ((a rem n) > (-n)) a:{...0}, n:. (0 (a rem n) ) & ((a rem n) > (-n)) 
Tx:A. B(x)
Q
A
B